a, b, c:. a + c + c  b  b + ((1/3) * c)  a  0 < c  False 

latex

Definitions

b, i <z j, r - s, qpositive(r), p q, q_le(r;s), <+>, t.1, , gset, goset, t.2, , x f y, p  q, a < b, a <p b, a < b, r < s, r + s, T, 1/r, True, (r/s), r * s, ff, (i = j), tt, if b then t else f fi , P & Q, P  Q, qeq(r;s), b, P  Q, A, , t  T, P  Q, x:A. B(x), {T}, False, S  T

Lemmas

qmul-ident-div, qmul preserves qle, qmul zero qrng, q distrib, qmul ident, qmul assoc, qadd inv assoc q, qadd ac 1 q, mon assoc q, qmul over plus qrng, qadd preserves qle, qinv inv q, mon ident q, qinverse q, qadd comm q, true wf, squash wf, qadd preserves qless, iff transitivity, qless transitivity 2 qorder, qle transitivity qorder, false wf, assert-qeq, qeq wf2, assert wf, rationals wf, not functionality wrt iff, qdiv wf, qmul wf, qadd wf, qle wf, int inc rationals, qless wf